the_w:World, l:IdLnk, t, t':.
(match(l;t;t'))
 ((||snds(l;t)||  ||rcvs(l;t')||)
 & (||rcvs(l;t')|| < (||snds(l;t)||+||onlnk(l;m(source(l);t))||))) 

latex

Definitions	x:A. B(x), match(l;t;t'), t  T, P  Q, Top, S  T, P  Q, P & Q, P  Q, , , Msg
Lemmas	nat wf, IdLnk wf, world wf, w-m wf, lsrc wf, Msg wf, w-M wf, Id wf, mlnk wf, length wf nat, w-onlnk wf, w-Msg wf, top wf, iff functionality wrt iff, assert wf, band wf, le int wf, length wf1, w-snds wf, w-action wf, ldst wf, w-rcvs wf, lt int wf, le wf, iff transitivity, assert of band, and functionality wrt iff, assert of le int, assert of lt int